\begin{tabbing}
$\forall$$R$:Realizer.
\\[0ex](R{-}size($R$) $\leq$ 1)
\\[0ex]$\Rightarrow$ \=($\forall$${\it ix}$:(:Id $\times$ Id).\+
\\[0ex]($\uparrow$${\it ix}$ $\in$ dom(R{-}discrete($R$)))
\\[0ex]$\Rightarrow$ (${\it ix}$ $\sim$ $<$R{-}loc($R$), if Reffect?($R$) then Reffect{-}x($R$) else Rinit{-}x($R$) fi $>$))
\-
\end{tabbing}